H-Termination proof of /home/matraf/haskell/eval_FullyBlown

YES 2.2600000000000002 H-Termination proof of /home/matraf/haskell/eval_FullyBlown_Fast/empty.hs
H-Termination of the given Haskell-Program with start terms could successfully be proven:

↳ HASKELL

  ↳ IFR

mainModule Main

((quotRem :: Int -> Int -> (Int,Int)) :: Int -> Int -> (Int,Int))

module Main where

import qualified Prelude

If Reductions:
The following If expression

if primGEqNatS x y then Succ (primDivNatS (primMinusNatS x y) (Succ y)) else Zero

is transformed to

primDivNatS0 x y True = Succ (primDivNatS (primMinusNatS x y) (Succ y))

primDivNatS0 x y False = Zero

The following If expression

if primGEqNatS x y then primModNatS (primMinusNatS x y) (Succ y) else Succ x

is transformed to

primModNatS0 x y True = primModNatS (primMinusNatS x y) (Succ y)

primModNatS0 x y False = Succ x

↳ HASKELL

  ↳ IFR

    ↳ HASKELL

      ↳ BR

mainModule Main

((quotRem :: Int -> Int -> (Int,Int)) :: Int -> Int -> (Int,Int))

module Main where

import qualified Prelude

Replaced joker patterns by fresh variables and removed binding patterns.

↳ HASKELL

  ↳ IFR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

mainModule Main

((quotRem :: Int -> Int -> (Int,Int)) :: Int -> Int -> (Int,Int))

module Main where

import qualified Prelude

Cond Reductions:
The following Function with conditions

undefined

| False

= undefined

is transformed to

undefined = undefined1

undefined0 True = undefined

undefined1 = undefined0 False

↳ HASKELL

  ↳ IFR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ Narrow

mainModule Main

(quotRem :: Int -> Int -> (Int,Int))

module Main where

import qualified Prelude

Haskell To QDPs

digraph dp_graph {
node [outthreshold=100, inthreshold=100];1[label="quotRem",fontsize=16,color="grey",shape="box"];1 -> 3[label="",style="dashed", color="grey", weight=3];
3[label="quotRem wv3",fontsize=16,color="grey",shape="box"];3 -> 4[label="",style="dashed", color="grey", weight=3];
4[label="quotRem wv3 wv4",fontsize=16,color="black",shape="triangle"];4 -> 5[label="",style="solid", color="black", weight=3];
5[label="primQrmInt wv3 wv4",fontsize=16,color="black",shape="box"];5 -> 6[label="",style="solid", color="black", weight=3];
6[label="(primQuotInt wv3 wv4,primRemInt wv3 wv4)",fontsize=16,color="green",shape="box"];6 -> 7[label="",style="dashed", color="green", weight=3];
6 -> 8[label="",style="dashed", color="green", weight=3];
7[label="primQuotInt wv3 wv4",fontsize=16,color="burlywood",shape="box"];667[label="wv3/Pos wv30",fontsize=10,color="white",style="solid",shape="box"];7 -> 667[label="",style="solid", color="burlywood", weight=9];
667 -> 9[label="",style="solid", color="burlywood", weight=3];
668[label="wv3/Neg wv30",fontsize=10,color="white",style="solid",shape="box"];7 -> 668[label="",style="solid", color="burlywood", weight=9];
668 -> 10[label="",style="solid", color="burlywood", weight=3];
8[label="primRemInt wv3 wv4",fontsize=16,color="burlywood",shape="box"];669[label="wv3/Pos wv30",fontsize=10,color="white",style="solid",shape="box"];8 -> 669[label="",style="solid", color="burlywood", weight=9];
669 -> 11[label="",style="solid", color="burlywood", weight=3];
670[label="wv3/Neg wv30",fontsize=10,color="white",style="solid",shape="box"];8 -> 670[label="",style="solid", color="burlywood", weight=9];
670 -> 12[label="",style="solid", color="burlywood", weight=3];
9[label="primQuotInt (Pos wv30) wv4",fontsize=16,color="burlywood",shape="box"];671[label="wv4/Pos wv40",fontsize=10,color="white",style="solid",shape="box"];9 -> 671[label="",style="solid", color="burlywood", weight=9];
671 -> 13[label="",style="solid", color="burlywood", weight=3];
672[label="wv4/Neg wv40",fontsize=10,color="white",style="solid",shape="box"];9 -> 672[label="",style="solid", color="burlywood", weight=9];
672 -> 14[label="",style="solid", color="burlywood", weight=3];
10[label="primQuotInt (Neg wv30) wv4",fontsize=16,color="burlywood",shape="box"];673[label="wv4/Pos wv40",fontsize=10,color="white",style="solid",shape="box"];10 -> 673[label="",style="solid", color="burlywood", weight=9];
673 -> 15[label="",style="solid", color="burlywood", weight=3];
674[label="wv4/Neg wv40",fontsize=10,color="white",style="solid",shape="box"];10 -> 674[label="",style="solid", color="burlywood", weight=9];
674 -> 16[label="",style="solid", color="burlywood", weight=3];
11[label="primRemInt (Pos wv30) wv4",fontsize=16,color="burlywood",shape="box"];675[label="wv4/Pos wv40",fontsize=10,color="white",style="solid",shape="box"];11 -> 675[label="",style="solid", color="burlywood", weight=9];
675 -> 17[label="",style="solid", color="burlywood", weight=3];
676[label="wv4/Neg wv40",fontsize=10,color="white",style="solid",shape="box"];11 -> 676[label="",style="solid", color="burlywood", weight=9];
676 -> 18[label="",style="solid", color="burlywood", weight=3];
12[label="primRemInt (Neg wv30) wv4",fontsize=16,color="burlywood",shape="box"];677[label="wv4/Pos wv40",fontsize=10,color="white",style="solid",shape="box"];12 -> 677[label="",style="solid", color="burlywood", weight=9];
677 -> 19[label="",style="solid", color="burlywood", weight=3];
678[label="wv4/Neg wv40",fontsize=10,color="white",style="solid",shape="box"];12 -> 678[label="",style="solid", color="burlywood", weight=9];
678 -> 20[label="",style="solid", color="burlywood", weight=3];
13[label="primQuotInt (Pos wv30) (Pos wv40)",fontsize=16,color="burlywood",shape="box"];679[label="wv40/Succ wv400",fontsize=10,color="white",style="solid",shape="box"];13 -> 679[label="",style="solid", color="burlywood", weight=9];
679 -> 21[label="",style="solid", color="burlywood", weight=3];
680[label="wv40/Zero",fontsize=10,color="white",style="solid",shape="box"];13 -> 680[label="",style="solid", color="burlywood", weight=9];
680 -> 22[label="",style="solid", color="burlywood", weight=3];
14[label="primQuotInt (Pos wv30) (Neg wv40)",fontsize=16,color="burlywood",shape="box"];681[label="wv40/Succ wv400",fontsize=10,color="white",style="solid",shape="box"];14 -> 681[label="",style="solid", color="burlywood", weight=9];
681 -> 23[label="",style="solid", color="burlywood", weight=3];
682[label="wv40/Zero",fontsize=10,color="white",style="solid",shape="box"];14 -> 682[label="",style="solid", color="burlywood", weight=9];
682 -> 24[label="",style="solid", color="burlywood", weight=3];
15[label="primQuotInt (Neg wv30) (Pos wv40)",fontsize=16,color="burlywood",shape="box"];683[label="wv40/Succ wv400",fontsize=10,color="white",style="solid",shape="box"];15 -> 683[label="",style="solid", color="burlywood", weight=9];
683 -> 25[label="",style="solid", color="burlywood", weight=3];
684[label="wv40/Zero",fontsize=10,color="white",style="solid",shape="box"];15 -> 684[label="",style="solid", color="burlywood", weight=9];
684 -> 26[label="",style="solid", color="burlywood", weight=3];
16[label="primQuotInt (Neg wv30) (Neg wv40)",fontsize=16,color="burlywood",shape="box"];685[label="wv40/Succ wv400",fontsize=10,color="white",style="solid",shape="box"];16 -> 685[label="",style="solid", color="burlywood", weight=9];
685 -> 27[label="",style="solid", color="burlywood", weight=3];
686[label="wv40/Zero",fontsize=10,color="white",style="solid",shape="box"];16 -> 686[label="",style="solid", color="burlywood", weight=9];
686 -> 28[label="",style="solid", color="burlywood", weight=3];
17[label="primRemInt (Pos wv30) (Pos wv40)",fontsize=16,color="burlywood",shape="box"];687[label="wv40/Succ wv400",fontsize=10,color="white",style="solid",shape="box"];17 -> 687[label="",style="solid", color="burlywood", weight=9];
687 -> 29[label="",style="solid", color="burlywood", weight=3];
688[label="wv40/Zero",fontsize=10,color="white",style="solid",shape="box"];17 -> 688[label="",style="solid", color="burlywood", weight=9];
688 -> 30[label="",style="solid", color="burlywood", weight=3];
18[label="primRemInt (Pos wv30) (Neg wv40)",fontsize=16,color="burlywood",shape="box"];689[label="wv40/Succ wv400",fontsize=10,color="white",style="solid",shape="box"];18 -> 689[label="",style="solid", color="burlywood", weight=9];
689 -> 31[label="",style="solid", color="burlywood", weight=3];
690[label="wv40/Zero",fontsize=10,color="white",style="solid",shape="box"];18 -> 690[label="",style="solid", color="burlywood", weight=9];
690 -> 32[label="",style="solid", color="burlywood", weight=3];
19[label="primRemInt (Neg wv30) (Pos wv40)",fontsize=16,color="burlywood",shape="box"];691[label="wv40/Succ wv400",fontsize=10,color="white",style="solid",shape="box"];19 -> 691[label="",style="solid", color="burlywood", weight=9];
691 -> 33[label="",style="solid", color="burlywood", weight=3];
692[label="wv40/Zero",fontsize=10,color="white",style="solid",shape="box"];19 -> 692[label="",style="solid", color="burlywood", weight=9];
692 -> 34[label="",style="solid", color="burlywood", weight=3];
20[label="primRemInt (Neg wv30) (Neg wv40)",fontsize=16,color="burlywood",shape="box"];693[label="wv40/Succ wv400",fontsize=10,color="white",style="solid",shape="box"];20 -> 693[label="",style="solid", color="burlywood", weight=9];
693 -> 35[label="",style="solid", color="burlywood", weight=3];
694[label="wv40/Zero",fontsize=10,color="white",style="solid",shape="box"];20 -> 694[label="",style="solid", color="burlywood", weight=9];
694 -> 36[label="",style="solid", color="burlywood", weight=3];
21[label="primQuotInt (Pos wv30) (Pos (Succ wv400))",fontsize=16,color="black",shape="box"];21 -> 37[label="",style="solid", color="black", weight=3];
22[label="primQuotInt (Pos wv30) (Pos Zero)",fontsize=16,color="black",shape="box"];22 -> 38[label="",style="solid", color="black", weight=3];
23[label="primQuotInt (Pos wv30) (Neg (Succ wv400))",fontsize=16,color="black",shape="box"];23 -> 39[label="",style="solid", color="black", weight=3];
24[label="primQuotInt (Pos wv30) (Neg Zero)",fontsize=16,color="black",shape="box"];24 -> 40[label="",style="solid", color="black", weight=3];
25[label="primQuotInt (Neg wv30) (Pos (Succ wv400))",fontsize=16,color="black",shape="box"];25 -> 41[label="",style="solid", color="black", weight=3];
26[label="primQuotInt (Neg wv30) (Pos Zero)",fontsize=16,color="black",shape="box"];26 -> 42[label="",style="solid", color="black", weight=3];
27[label="primQuotInt (Neg wv30) (Neg (Succ wv400))",fontsize=16,color="black",shape="box"];27 -> 43[label="",style="solid", color="black", weight=3];
28[label="primQuotInt (Neg wv30) (Neg Zero)",fontsize=16,color="black",shape="box"];28 -> 44[label="",style="solid", color="black", weight=3];
29[label="primRemInt (Pos wv30) (Pos (Succ wv400))",fontsize=16,color="black",shape="box"];29 -> 45[label="",style="solid", color="black", weight=3];
30[label="primRemInt (Pos wv30) (Pos Zero)",fontsize=16,color="black",shape="box"];30 -> 46[label="",style="solid", color="black", weight=3];
31[label="primRemInt (Pos wv30) (Neg (Succ wv400))",fontsize=16,color="black",shape="box"];31 -> 47[label="",style="solid", color="black", weight=3];
32[label="primRemInt (Pos wv30) (Neg Zero)",fontsize=16,color="black",shape="box"];32 -> 48[label="",style="solid", color="black", weight=3];
33[label="primRemInt (Neg wv30) (Pos (Succ wv400))",fontsize=16,color="black",shape="box"];33 -> 49[label="",style="solid", color="black", weight=3];
34[label="primRemInt (Neg wv30) (Pos Zero)",fontsize=16,color="black",shape="box"];34 -> 50[label="",style="solid", color="black", weight=3];
35[label="primRemInt (Neg wv30) (Neg (Succ wv400))",fontsize=16,color="black",shape="box"];35 -> 51[label="",style="solid", color="black", weight=3];
36[label="primRemInt (Neg wv30) (Neg Zero)",fontsize=16,color="black",shape="box"];36 -> 52[label="",style="solid", color="black", weight=3];
37[label="Pos (primDivNatS wv30 (Succ wv400))",fontsize=16,color="green",shape="box"];37 -> 53[label="",style="dashed", color="green", weight=3];
38[label="error []",fontsize=16,color="black",shape="triangle"];38 -> 54[label="",style="solid", color="black", weight=3];
39[label="Neg (primDivNatS wv30 (Succ wv400))",fontsize=16,color="green",shape="box"];39 -> 55[label="",style="dashed", color="green", weight=3];
40 -> 38[label="",style="dashed", color="red", weight=0];
40[label="error []",fontsize=16,color="magenta"];41[label="Neg (primDivNatS wv30 (Succ wv400))",fontsize=16,color="green",shape="box"];41 -> 56[label="",style="dashed", color="green", weight=3];
42 -> 38[label="",style="dashed", color="red", weight=0];
42[label="error []",fontsize=16,color="magenta"];43[label="Pos (primDivNatS wv30 (Succ wv400))",fontsize=16,color="green",shape="box"];43 -> 57[label="",style="dashed", color="green", weight=3];
44 -> 38[label="",style="dashed", color="red", weight=0];
44[label="error []",fontsize=16,color="magenta"];45[label="Pos (primModNatS wv30 (Succ wv400))",fontsize=16,color="green",shape="box"];45 -> 58[label="",style="dashed", color="green", weight=3];
46 -> 38[label="",style="dashed", color="red", weight=0];
46[label="error []",fontsize=16,color="magenta"];47[label="Pos (primModNatS wv30 (Succ wv400))",fontsize=16,color="green",shape="box"];47 -> 59[label="",style="dashed", color="green", weight=3];
48 -> 38[label="",style="dashed", color="red", weight=0];
48[label="error []",fontsize=16,color="magenta"];49[label="Neg (primModNatS wv30 (Succ wv400))",fontsize=16,color="green",shape="box"];49 -> 60[label="",style="dashed", color="green", weight=3];
50 -> 38[label="",style="dashed", color="red", weight=0];
50[label="error []",fontsize=16,color="magenta"];51[label="Neg (primModNatS wv30 (Succ wv400))",fontsize=16,color="green",shape="box"];51 -> 61[label="",style="dashed", color="green", weight=3];
52 -> 38[label="",style="dashed", color="red", weight=0];
52[label="error []",fontsize=16,color="magenta"];53[label="primDivNatS wv30 (Succ wv400)",fontsize=16,color="burlywood",shape="triangle"];702[label="wv30/Succ wv300",fontsize=10,color="white",style="solid",shape="box"];53 -> 702[label="",style="solid", color="burlywood", weight=9];
702 -> 62[label="",style="solid", color="burlywood", weight=3];
703[label="wv30/Zero",fontsize=10,color="white",style="solid",shape="box"];53 -> 703[label="",style="solid", color="burlywood", weight=9];
703 -> 63[label="",style="solid", color="burlywood", weight=3];
54[label="error []",fontsize=16,color="red",shape="box"];55 -> 53[label="",style="dashed", color="red", weight=0];
55[label="primDivNatS wv30 (Succ wv400)",fontsize=16,color="magenta"];55 -> 64[label="",style="dashed", color="magenta", weight=3];
56 -> 53[label="",style="dashed", color="red", weight=0];
56[label="primDivNatS wv30 (Succ wv400)",fontsize=16,color="magenta"];56 -> 65[label="",style="dashed", color="magenta", weight=3];
57 -> 53[label="",style="dashed", color="red", weight=0];
57[label="primDivNatS wv30 (Succ wv400)",fontsize=16,color="magenta"];57 -> 66[label="",style="dashed", color="magenta", weight=3];
57 -> 67[label="",style="dashed", color="magenta", weight=3];
58[label="primModNatS wv30 (Succ wv400)",fontsize=16,color="burlywood",shape="triangle"];707[label="wv30/Succ wv300",fontsize=10,color="white",style="solid",shape="box"];58 -> 707[label="",style="solid", color="burlywood", weight=9];
707 -> 68[label="",style="solid", color="burlywood", weight=3];
708[label="wv30/Zero",fontsize=10,color="white",style="solid",shape="box"];58 -> 708[label="",style="solid", color="burlywood", weight=9];
708 -> 69[label="",style="solid", color="burlywood", weight=3];
59 -> 58[label="",style="dashed", color="red", weight=0];
59[label="primModNatS wv30 (Succ wv400)",fontsize=16,color="magenta"];59 -> 70[label="",style="dashed", color="magenta", weight=3];
60 -> 58[label="",style="dashed", color="red", weight=0];
60[label="primModNatS wv30 (Succ wv400)",fontsize=16,color="magenta"];60 -> 71[label="",style="dashed", color="magenta", weight=3];
61 -> 58[label="",style="dashed", color="red", weight=0];
61[label="primModNatS wv30 (Succ wv400)",fontsize=16,color="magenta"];61 -> 72[label="",style="dashed", color="magenta", weight=3];
61 -> 73[label="",style="dashed", color="magenta", weight=3];
62[label="primDivNatS (Succ wv300) (Succ wv400)",fontsize=16,color="black",shape="box"];62 -> 74[label="",style="solid", color="black", weight=3];
63[label="primDivNatS Zero (Succ wv400)",fontsize=16,color="black",shape="box"];63 -> 75[label="",style="solid", color="black", weight=3];
64[label="wv400",fontsize=16,color="green",shape="box"];65[label="wv30",fontsize=16,color="green",shape="box"];66[label="wv400",fontsize=16,color="green",shape="box"];67[label="wv30",fontsize=16,color="green",shape="box"];68[label="primModNatS (Succ wv300) (Succ wv400)",fontsize=16,color="black",shape="box"];68 -> 76[label="",style="solid", color="black", weight=3];
69[label="primModNatS Zero (Succ wv400)",fontsize=16,color="black",shape="box"];69 -> 77[label="",style="solid", color="black", weight=3];
70[label="wv400",fontsize=16,color="green",shape="box"];71[label="wv30",fontsize=16,color="green",shape="box"];72[label="wv400",fontsize=16,color="green",shape="box"];73[label="wv30",fontsize=16,color="green",shape="box"];74[label="primDivNatS0 wv300 wv400 (primGEqNatS wv300 wv400)",fontsize=16,color="burlywood",shape="box"];712[label="wv300/Succ wv3000",fontsize=10,color="white",style="solid",shape="box"];74 -> 712[label="",style="solid", color="burlywood", weight=9];
712 -> 78[label="",style="solid", color="burlywood", weight=3];
713[label="wv300/Zero",fontsize=10,color="white",style="solid",shape="box"];74 -> 713[label="",style="solid", color="burlywood", weight=9];
713 -> 79[label="",style="solid", color="burlywood", weight=3];
75[label="Zero",fontsize=16,color="green",shape="box"];76[label="primModNatS0 wv300 wv400 (primGEqNatS wv300 wv400)",fontsize=16,color="burlywood",shape="box"];714[label="wv300/Succ wv3000",fontsize=10,color="white",style="solid",shape="box"];76 -> 714[label="",style="solid", color="burlywood", weight=9];
714 -> 80[label="",style="solid", color="burlywood", weight=3];
715[label="wv300/Zero",fontsize=10,color="white",style="solid",shape="box"];76 -> 715[label="",style="solid", color="burlywood", weight=9];
715 -> 81[label="",style="solid", color="burlywood", weight=3];
77[label="Zero",fontsize=16,color="green",shape="box"];78[label="primDivNatS0 (Succ wv3000) wv400 (primGEqNatS (Succ wv3000) wv400)",fontsize=16,color="burlywood",shape="box"];716[label="wv400/Succ wv4000",fontsize=10,color="white",style="solid",shape="box"];78 -> 716[label="",style="solid", color="burlywood", weight=9];
716 -> 82[label="",style="solid", color="burlywood", weight=3];
717[label="wv400/Zero",fontsize=10,color="white",style="solid",shape="box"];78 -> 717[label="",style="solid", color="burlywood", weight=9];
717 -> 83[label="",style="solid", color="burlywood", weight=3];
79[label="primDivNatS0 Zero wv400 (primGEqNatS Zero wv400)",fontsize=16,color="burlywood",shape="box"];718[label="wv400/Succ wv4000",fontsize=10,color="white",style="solid",shape="box"];79 -> 718[label="",style="solid", color="burlywood", weight=9];
718 -> 84[label="",style="solid", color="burlywood", weight=3];
719[label="wv400/Zero",fontsize=10,color="white",style="solid",shape="box"];79 -> 719[label="",style="solid", color="burlywood", weight=9];
719 -> 85[label="",style="solid", color="burlywood", weight=3];
80[label="primModNatS0 (Succ wv3000) wv400 (primGEqNatS (Succ wv3000) wv400)",fontsize=16,color="burlywood",shape="box"];720[label="wv400/Succ wv4000",fontsize=10,color="white",style="solid",shape="box"];80 -> 720[label="",style="solid", color="burlywood", weight=9];
720 -> 86[label="",style="solid", color="burlywood", weight=3];
721[label="wv400/Zero",fontsize=10,color="white",style="solid",shape="box"];80 -> 721[label="",style="solid", color="burlywood", weight=9];
721 -> 87[label="",style="solid", color="burlywood", weight=3];
81[label="primModNatS0 Zero wv400 (primGEqNatS Zero wv400)",fontsize=16,color="burlywood",shape="box"];722[label="wv400/Succ wv4000",fontsize=10,color="white",style="solid",shape="box"];81 -> 722[label="",style="solid", color="burlywood", weight=9];
722 -> 88[label="",style="solid", color="burlywood", weight=3];
723[label="wv400/Zero",fontsize=10,color="white",style="solid",shape="box"];81 -> 723[label="",style="solid", color="burlywood", weight=9];
723 -> 89[label="",style="solid", color="burlywood", weight=3];
82[label="primDivNatS0 (Succ wv3000) (Succ wv4000) (primGEqNatS (Succ wv3000) (Succ wv4000))",fontsize=16,color="black",shape="box"];82 -> 90[label="",style="solid", color="black", weight=3];
83[label="primDivNatS0 (Succ wv3000) Zero (primGEqNatS (Succ wv3000) Zero)",fontsize=16,color="black",shape="box"];83 -> 91[label="",style="solid", color="black", weight=3];
84[label="primDivNatS0 Zero (Succ wv4000) (primGEqNatS Zero (Succ wv4000))",fontsize=16,color="black",shape="box"];84 -> 92[label="",style="solid", color="black", weight=3];
85[label="primDivNatS0 Zero Zero (primGEqNatS Zero Zero)",fontsize=16,color="black",shape="box"];85 -> 93[label="",style="solid", color="black", weight=3];
86[label="primModNatS0 (Succ wv3000) (Succ wv4000) (primGEqNatS (Succ wv3000) (Succ wv4000))",fontsize=16,color="black",shape="box"];86 -> 94[label="",style="solid", color="black", weight=3];
87[label="primModNatS0 (Succ wv3000) Zero (primGEqNatS (Succ wv3000) Zero)",fontsize=16,color="black",shape="box"];87 -> 95[label="",style="solid", color="black", weight=3];
88[label="primModNatS0 Zero (Succ wv4000) (primGEqNatS Zero (Succ wv4000))",fontsize=16,color="black",shape="box"];88 -> 96[label="",style="solid", color="black", weight=3];
89[label="primModNatS0 Zero Zero (primGEqNatS Zero Zero)",fontsize=16,color="black",shape="box"];89 -> 97[label="",style="solid", color="black", weight=3];
90 -> 535[label="",style="dashed", color="red", weight=0];
90[label="primDivNatS0 (Succ wv3000) (Succ wv4000) (primGEqNatS wv3000 wv4000)",fontsize=16,color="magenta"];90 -> 536[label="",style="dashed", color="magenta", weight=3];
90 -> 537[label="",style="dashed", color="magenta", weight=3];
90 -> 538[label="",style="dashed", color="magenta", weight=3];
90 -> 539[label="",style="dashed", color="magenta", weight=3];
91[label="primDivNatS0 (Succ wv3000) Zero True",fontsize=16,color="black",shape="box"];91 -> 100[label="",style="solid", color="black", weight=3];
92[label="primDivNatS0 Zero (Succ wv4000) False",fontsize=16,color="black",shape="box"];92 -> 101[label="",style="solid", color="black", weight=3];
93[label="primDivNatS0 Zero Zero True",fontsize=16,color="black",shape="box"];93 -> 102[label="",style="solid", color="black", weight=3];
94 -> 580[label="",style="dashed", color="red", weight=0];
94[label="primModNatS0 (Succ wv3000) (Succ wv4000) (primGEqNatS wv3000 wv4000)",fontsize=16,color="magenta"];94 -> 581[label="",style="dashed", color="magenta", weight=3];
94 -> 582[label="",style="dashed", color="magenta", weight=3];
94 -> 583[label="",style="dashed", color="magenta", weight=3];
94 -> 584[label="",style="dashed", color="magenta", weight=3];
95[label="primModNatS0 (Succ wv3000) Zero True",fontsize=16,color="black",shape="box"];95 -> 105[label="",style="solid", color="black", weight=3];
96[label="primModNatS0 Zero (Succ wv4000) False",fontsize=16,color="black",shape="box"];96 -> 106[label="",style="solid", color="black", weight=3];
97[label="primModNatS0 Zero Zero True",fontsize=16,color="black",shape="box"];97 -> 107[label="",style="solid", color="black", weight=3];
536[label="wv3000",fontsize=16,color="green",shape="box"];537[label="wv3000",fontsize=16,color="green",shape="box"];538[label="wv4000",fontsize=16,color="green",shape="box"];539[label="wv4000",fontsize=16,color="green",shape="box"];535[label="primDivNatS0 (Succ wv46) (Succ wv47) (primGEqNatS wv48 wv49)",fontsize=16,color="burlywood",shape="triangle"];726[label="wv48/Succ wv480",fontsize=10,color="white",style="solid",shape="box"];535 -> 726[label="",style="solid", color="burlywood", weight=9];
726 -> 576[label="",style="solid", color="burlywood", weight=3];
727[label="wv48/Zero",fontsize=10,color="white",style="solid",shape="box"];535 -> 727[label="",style="solid", color="burlywood", weight=9];
727 -> 577[label="",style="solid", color="burlywood", weight=3];
100[label="Succ (primDivNatS (primMinusNatS (Succ wv3000) Zero) (Succ Zero))",fontsize=16,color="green",shape="box"];100 -> 112[label="",style="dashed", color="green", weight=3];
101[label="Zero",fontsize=16,color="green",shape="box"];102[label="Succ (primDivNatS (primMinusNatS Zero Zero) (Succ Zero))",fontsize=16,color="green",shape="box"];102 -> 113[label="",style="dashed", color="green", weight=3];
581[label="wv4000",fontsize=16,color="green",shape="box"];582[label="wv4000",fontsize=16,color="green",shape="box"];583[label="wv3000",fontsize=16,color="green",shape="box"];584[label="wv3000",fontsize=16,color="green",shape="box"];580[label="primModNatS0 (Succ wv51) (Succ wv52) (primGEqNatS wv53 wv54)",fontsize=16,color="burlywood",shape="triangle"];728[label="wv53/Succ wv530",fontsize=10,color="white",style="solid",shape="box"];580 -> 728[label="",style="solid", color="burlywood", weight=9];
728 -> 621[label="",style="solid", color="burlywood", weight=3];
729[label="wv53/Zero",fontsize=10,color="white",style="solid",shape="box"];580 -> 729[label="",style="solid", color="burlywood", weight=9];
729 -> 622[label="",style="solid", color="burlywood", weight=3];
105 -> 58[label="",style="dashed", color="red", weight=0];
105[label="primModNatS (primMinusNatS (Succ wv3000) Zero) (Succ Zero)",fontsize=16,color="magenta"];105 -> 118[label="",style="dashed", color="magenta", weight=3];
105 -> 119[label="",style="dashed", color="magenta", weight=3];
106[label="Succ Zero",fontsize=16,color="green",shape="box"];107 -> 58[label="",style="dashed", color="red", weight=0];
107[label="primModNatS (primMinusNatS Zero Zero) (Succ Zero)",fontsize=16,color="magenta"];107 -> 120[label="",style="dashed", color="magenta", weight=3];
107 -> 121[label="",style="dashed", color="magenta", weight=3];
576[label="primDivNatS0 (Succ wv46) (Succ wv47) (primGEqNatS (Succ wv480) wv49)",fontsize=16,color="burlywood",shape="box"];732[label="wv49/Succ wv490",fontsize=10,color="white",style="solid",shape="box"];576 -> 732[label="",style="solid", color="burlywood", weight=9];
732 -> 623[label="",style="solid", color="burlywood", weight=3];
733[label="wv49/Zero",fontsize=10,color="white",style="solid",shape="box"];576 -> 733[label="",style="solid", color="burlywood", weight=9];
733 -> 624[label="",style="solid", color="burlywood", weight=3];
577[label="primDivNatS0 (Succ wv46) (Succ wv47) (primGEqNatS Zero wv49)",fontsize=16,color="burlywood",shape="box"];734[label="wv49/Succ wv490",fontsize=10,color="white",style="solid",shape="box"];577 -> 734[label="",style="solid", color="burlywood", weight=9];
734 -> 625[label="",style="solid", color="burlywood", weight=3];
735[label="wv49/Zero",fontsize=10,color="white",style="solid",shape="box"];577 -> 735[label="",style="solid", color="burlywood", weight=9];
735 -> 626[label="",style="solid", color="burlywood", weight=3];
112 -> 53[label="",style="dashed", color="red", weight=0];
112[label="primDivNatS (primMinusNatS (Succ wv3000) Zero) (Succ Zero)",fontsize=16,color="magenta"];112 -> 126[label="",style="dashed", color="magenta", weight=3];
112 -> 127[label="",style="dashed", color="magenta", weight=3];
113 -> 53[label="",style="dashed", color="red", weight=0];
113[label="primDivNatS (primMinusNatS Zero Zero) (Succ Zero)",fontsize=16,color="magenta"];113 -> 128[label="",style="dashed", color="magenta", weight=3];
113 -> 129[label="",style="dashed", color="magenta", weight=3];
621[label="primModNatS0 (Succ wv51) (Succ wv52) (primGEqNatS (Succ wv530) wv54)",fontsize=16,color="burlywood",shape="box"];738[label="wv54/Succ wv540",fontsize=10,color="white",style="solid",shape="box"];621 -> 738[label="",style="solid", color="burlywood", weight=9];
738 -> 627[label="",style="solid", color="burlywood", weight=3];
739[label="wv54/Zero",fontsize=10,color="white",style="solid",shape="box"];621 -> 739[label="",style="solid", color="burlywood", weight=9];
739 -> 628[label="",style="solid", color="burlywood", weight=3];
622[label="primModNatS0 (Succ wv51) (Succ wv52) (primGEqNatS Zero wv54)",fontsize=16,color="burlywood",shape="box"];740[label="wv54/Succ wv540",fontsize=10,color="white",style="solid",shape="box"];622 -> 740[label="",style="solid", color="burlywood", weight=9];
740 -> 629[label="",style="solid", color="burlywood", weight=3];
741[label="wv54/Zero",fontsize=10,color="white",style="solid",shape="box"];622 -> 741[label="",style="solid", color="burlywood", weight=9];
741 -> 630[label="",style="solid", color="burlywood", weight=3];
118[label="Zero",fontsize=16,color="green",shape="box"];119[label="primMinusNatS (Succ wv3000) Zero",fontsize=16,color="black",shape="triangle"];119 -> 134[label="",style="solid", color="black", weight=3];
120[label="Zero",fontsize=16,color="green",shape="box"];121[label="primMinusNatS Zero Zero",fontsize=16,color="black",shape="triangle"];121 -> 135[label="",style="solid", color="black", weight=3];
623[label="primDivNatS0 (Succ wv46) (Succ wv47) (primGEqNatS (Succ wv480) (Succ wv490))",fontsize=16,color="black",shape="box"];623 -> 631[label="",style="solid", color="black", weight=3];
624[label="primDivNatS0 (Succ wv46) (Succ wv47) (primGEqNatS (Succ wv480) Zero)",fontsize=16,color="black",shape="box"];624 -> 632[label="",style="solid", color="black", weight=3];
625[label="primDivNatS0 (Succ wv46) (Succ wv47) (primGEqNatS Zero (Succ wv490))",fontsize=16,color="black",shape="box"];625 -> 633[label="",style="solid", color="black", weight=3];
626[label="primDivNatS0 (Succ wv46) (Succ wv47) (primGEqNatS Zero Zero)",fontsize=16,color="black",shape="box"];626 -> 634[label="",style="solid", color="black", weight=3];
126[label="Zero",fontsize=16,color="green",shape="box"];127 -> 119[label="",style="dashed", color="red", weight=0];
127[label="primMinusNatS (Succ wv3000) Zero",fontsize=16,color="magenta"];128[label="Zero",fontsize=16,color="green",shape="box"];129 -> 121[label="",style="dashed", color="red", weight=0];
129[label="primMinusNatS Zero Zero",fontsize=16,color="magenta"];627[label="primModNatS0 (Succ wv51) (Succ wv52) (primGEqNatS (Succ wv530) (Succ wv540))",fontsize=16,color="black",shape="box"];627 -> 635[label="",style="solid", color="black", weight=3];
628[label="primModNatS0 (Succ wv51) (Succ wv52) (primGEqNatS (Succ wv530) Zero)",fontsize=16,color="black",shape="box"];628 -> 636[label="",style="solid", color="black", weight=3];
629[label="primModNatS0 (Succ wv51) (Succ wv52) (primGEqNatS Zero (Succ wv540))",fontsize=16,color="black",shape="box"];629 -> 637[label="",style="solid", color="black", weight=3];
630[label="primModNatS0 (Succ wv51) (Succ wv52) (primGEqNatS Zero Zero)",fontsize=16,color="black",shape="box"];630 -> 638[label="",style="solid", color="black", weight=3];
134[label="Succ wv3000",fontsize=16,color="green",shape="box"];135[label="Zero",fontsize=16,color="green",shape="box"];631 -> 535[label="",style="dashed", color="red", weight=0];
631[label="primDivNatS0 (Succ wv46) (Succ wv47) (primGEqNatS wv480 wv490)",fontsize=16,color="magenta"];631 -> 639[label="",style="dashed", color="magenta", weight=3];
631 -> 640[label="",style="dashed", color="magenta", weight=3];
632[label="primDivNatS0 (Succ wv46) (Succ wv47) True",fontsize=16,color="black",shape="triangle"];632 -> 641[label="",style="solid", color="black", weight=3];
633[label="primDivNatS0 (Succ wv46) (Succ wv47) False",fontsize=16,color="black",shape="box"];633 -> 642[label="",style="solid", color="black", weight=3];
634 -> 632[label="",style="dashed", color="red", weight=0];
634[label="primDivNatS0 (Succ wv46) (Succ wv47) True",fontsize=16,color="magenta"];635 -> 580[label="",style="dashed", color="red", weight=0];
635[label="primModNatS0 (Succ wv51) (Succ wv52) (primGEqNatS wv530 wv540)",fontsize=16,color="magenta"];635 -> 643[label="",style="dashed", color="magenta", weight=3];
635 -> 644[label="",style="dashed", color="magenta", weight=3];
636[label="primModNatS0 (Succ wv51) (Succ wv52) True",fontsize=16,color="black",shape="triangle"];636 -> 645[label="",style="solid", color="black", weight=3];
637[label="primModNatS0 (Succ wv51) (Succ wv52) False",fontsize=16,color="black",shape="box"];637 -> 646[label="",style="solid", color="black", weight=3];
638 -> 636[label="",style="dashed", color="red", weight=0];
638[label="primModNatS0 (Succ wv51) (Succ wv52) True",fontsize=16,color="magenta"];639[label="wv480",fontsize=16,color="green",shape="box"];640[label="wv490",fontsize=16,color="green",shape="box"];641[label="Succ (primDivNatS (primMinusNatS (Succ wv46) (Succ wv47)) (Succ (Succ wv47)))",fontsize=16,color="green",shape="box"];641 -> 647[label="",style="dashed", color="green", weight=3];
642[label="Zero",fontsize=16,color="green",shape="box"];643[label="wv540",fontsize=16,color="green",shape="box"];644[label="wv530",fontsize=16,color="green",shape="box"];645 -> 58[label="",style="dashed", color="red", weight=0];
645[label="primModNatS (primMinusNatS (Succ wv51) (Succ wv52)) (Succ (Succ wv52))",fontsize=16,color="magenta"];645 -> 648[label="",style="dashed", color="magenta", weight=3];
645 -> 649[label="",style="dashed", color="magenta", weight=3];
646[label="Succ (Succ wv51)",fontsize=16,color="green",shape="box"];647 -> 53[label="",style="dashed", color="red", weight=0];
647[label="primDivNatS (primMinusNatS (Succ wv46) (Succ wv47)) (Succ (Succ wv47))",fontsize=16,color="magenta"];647 -> 650[label="",style="dashed", color="magenta", weight=3];
647 -> 651[label="",style="dashed", color="magenta", weight=3];
648[label="Succ wv52",fontsize=16,color="green",shape="box"];649[label="primMinusNatS (Succ wv51) (Succ wv52)",fontsize=16,color="black",shape="triangle"];649 -> 652[label="",style="solid", color="black", weight=3];
650[label="Succ wv47",fontsize=16,color="green",shape="box"];651 -> 649[label="",style="dashed", color="red", weight=0];
651[label="primMinusNatS (Succ wv46) (Succ wv47)",fontsize=16,color="magenta"];651 -> 653[label="",style="dashed", color="magenta", weight=3];
651 -> 654[label="",style="dashed", color="magenta", weight=3];
652[label="primMinusNatS wv51 wv52",fontsize=16,color="burlywood",shape="triangle"];751[label="wv51/Succ wv510",fontsize=10,color="white",style="solid",shape="box"];652 -> 751[label="",style="solid", color="burlywood", weight=9];
751 -> 655[label="",style="solid", color="burlywood", weight=3];
752[label="wv51/Zero",fontsize=10,color="white",style="solid",shape="box"];652 -> 752[label="",style="solid", color="burlywood", weight=9];
752 -> 656[label="",style="solid", color="burlywood", weight=3];
653[label="wv47",fontsize=16,color="green",shape="box"];654[label="wv46",fontsize=16,color="green",shape="box"];655[label="primMinusNatS (Succ wv510) wv52",fontsize=16,color="burlywood",shape="box"];753[label="wv52/Succ wv520",fontsize=10,color="white",style="solid",shape="box"];655 -> 753[label="",style="solid", color="burlywood", weight=9];
753 -> 657[label="",style="solid", color="burlywood", weight=3];
754[label="wv52/Zero",fontsize=10,color="white",style="solid",shape="box"];655 -> 754[label="",style="solid", color="burlywood", weight=9];
754 -> 658[label="",style="solid", color="burlywood", weight=3];
656[label="primMinusNatS Zero wv52",fontsize=16,color="burlywood",shape="box"];755[label="wv52/Succ wv520",fontsize=10,color="white",style="solid",shape="box"];656 -> 755[label="",style="solid", color="burlywood", weight=9];
755 -> 659[label="",style="solid", color="burlywood", weight=3];
756[label="wv52/Zero",fontsize=10,color="white",style="solid",shape="box"];656 -> 756[label="",style="solid", color="burlywood", weight=9];
756 -> 660[label="",style="solid", color="burlywood", weight=3];
657[label="primMinusNatS (Succ wv510) (Succ wv520)",fontsize=16,color="black",shape="box"];657 -> 661[label="",style="solid", color="black", weight=3];
658[label="primMinusNatS (Succ wv510) Zero",fontsize=16,color="black",shape="box"];658 -> 662[label="",style="solid", color="black", weight=3];
659[label="primMinusNatS Zero (Succ wv520)",fontsize=16,color="black",shape="box"];659 -> 663[label="",style="solid", color="black", weight=3];
660[label="primMinusNatS Zero Zero",fontsize=16,color="black",shape="box"];660 -> 664[label="",style="solid", color="black", weight=3];
661 -> 652[label="",style="dashed", color="red", weight=0];
661[label="primMinusNatS wv510 wv520",fontsize=16,color="magenta"];661 -> 665[label="",style="dashed", color="magenta", weight=3];
661 -> 666[label="",style="dashed", color="magenta", weight=3];
662[label="Succ wv510",fontsize=16,color="green",shape="box"];663[label="Zero",fontsize=16,color="green",shape="box"];664[label="Zero",fontsize=16,color="green",shape="box"];665[label="wv520",fontsize=16,color="green",shape="box"];666[label="wv510",fontsize=16,color="green",shape="box"];}

↳ HASKELL

  ↳ IFR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ Narrow

                ↳ AND

                  ↳ QDP

                    ↳ QDPSizeChangeProof

                  ↳ QDP

                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primMinusNatS(Succ(wv510), Succ(wv520)) → new_primMinusNatS(wv510, wv520)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

new_primMinusNatS(Succ(wv510), Succ(wv520)) → new_primMinusNatS(wv510, wv520)
The graph contains the following edges 1 > 1, 2 > 2

↳ HASKELL

  ↳ IFR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ Narrow

                ↳ AND

                  ↳ QDP

                  ↳ QDP

                    ↳ DependencyGraphProof

                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primModNatS0(wv51, wv52, Succ(wv530), Zero) → new_primModNatS(new_primMinusNatS2(wv51, wv52), Succ(wv52))
new_primModNatS00(wv51, wv52) → new_primModNatS(new_primMinusNatS2(wv51, wv52), Succ(wv52))
new_primModNatS(Succ(Zero), Zero) → new_primModNatS(new_primMinusNatS1, Zero)
new_primModNatS(Succ(Succ(wv3000)), Succ(wv4000)) → new_primModNatS0(wv3000, wv4000, wv3000, wv4000)
new_primModNatS(Succ(Succ(wv3000)), Zero) → new_primModNatS(new_primMinusNatS0(wv3000), Zero)
new_primModNatS0(wv51, wv52, Succ(wv530), Succ(wv540)) → new_primModNatS0(wv51, wv52, wv530, wv540)
new_primModNatS0(wv51, wv52, Zero, Zero) → new_primModNatS00(wv51, wv52)

The TRS R consists of the following rules:

new_primMinusNatS3(Zero, Succ(wv520)) → Zero
new_primMinusNatS3(Succ(wv510), Succ(wv520)) → new_primMinusNatS3(wv510, wv520)
new_primMinusNatS1 → Zero
new_primMinusNatS2(wv51, wv52) → new_primMinusNatS3(wv51, wv52)
new_primMinusNatS3(Zero, Zero) → Zero
new_primMinusNatS0(wv3000) → Succ(wv3000)
new_primMinusNatS3(Succ(wv510), Zero) → Succ(wv510)

The set Q consists of the following terms:

new_primMinusNatS3(Zero, Zero)
new_primMinusNatS3(Succ(x0), Zero)
new_primMinusNatS0(x0)
new_primMinusNatS2(x0, x1)
new_primMinusNatS3(Succ(x0), Succ(x1))
new_primMinusNatS1
new_primMinusNatS3(Zero, Succ(x0))

We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 2 SCCs with 1 less node.

↳ HASKELL

  ↳ IFR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ Narrow

                ↳ AND

                  ↳ QDP

                  ↳ QDP

                    ↳ DependencyGraphProof

                      ↳ AND

                        ↳ QDP

                          ↳ UsableRulesProof

                        ↳ QDP

                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primModNatS(Succ(Succ(wv3000)), Zero) → new_primModNatS(new_primMinusNatS0(wv3000), Zero)

The TRS R consists of the following rules:

new_primMinusNatS3(Zero, Succ(wv520)) → Zero
new_primMinusNatS3(Succ(wv510), Succ(wv520)) → new_primMinusNatS3(wv510, wv520)
new_primMinusNatS1 → Zero
new_primMinusNatS2(wv51, wv52) → new_primMinusNatS3(wv51, wv52)
new_primMinusNatS3(Zero, Zero) → Zero
new_primMinusNatS0(wv3000) → Succ(wv3000)
new_primMinusNatS3(Succ(wv510), Zero) → Succ(wv510)

The set Q consists of the following terms:

new_primMinusNatS3(Zero, Zero)
new_primMinusNatS3(Succ(x0), Zero)
new_primMinusNatS0(x0)
new_primMinusNatS2(x0, x1)
new_primMinusNatS3(Succ(x0), Succ(x1))
new_primMinusNatS1
new_primMinusNatS3(Zero, Succ(x0))

We have to consider all minimal (P,Q,R)-chains.
As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [15] we can delete all non-usable rules [17] from R.

↳ HASKELL

  ↳ IFR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ Narrow

                ↳ AND

                  ↳ QDP

                  ↳ QDP

                    ↳ DependencyGraphProof

                      ↳ AND

                        ↳ QDP

                          ↳ UsableRulesProof

                            ↳ QDP

                              ↳ QReductionProof

                        ↳ QDP

                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primModNatS(Succ(Succ(wv3000)), Zero) → new_primModNatS(new_primMinusNatS0(wv3000), Zero)

The TRS R consists of the following rules:

new_primMinusNatS0(wv3000) → Succ(wv3000)

The set Q consists of the following terms:

new_primMinusNatS3(Zero, Zero)
new_primMinusNatS3(Succ(x0), Zero)
new_primMinusNatS0(x0)
new_primMinusNatS2(x0, x1)
new_primMinusNatS3(Succ(x0), Succ(x1))
new_primMinusNatS1
new_primMinusNatS3(Zero, Succ(x0))

We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.

new_primMinusNatS3(Zero, Zero)
new_primMinusNatS3(Succ(x0), Zero)
new_primMinusNatS2(x0, x1)
new_primMinusNatS3(Succ(x0), Succ(x1))
new_primMinusNatS1
new_primMinusNatS3(Zero, Succ(x0))

↳ HASKELL

  ↳ IFR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ Narrow

                ↳ AND

                  ↳ QDP

                  ↳ QDP

                    ↳ DependencyGraphProof

                      ↳ AND

                        ↳ QDP

                          ↳ UsableRulesProof

                            ↳ QDP

                              ↳ QReductionProof

                                ↳ QDP

                                  ↳ RuleRemovalProof

                        ↳ QDP

                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primModNatS(Succ(Succ(wv3000)), Zero) → new_primModNatS(new_primMinusNatS0(wv3000), Zero)

The TRS R consists of the following rules:

new_primMinusNatS0(wv3000) → Succ(wv3000)

The set Q consists of the following terms:

new_primMinusNatS0(x0)

We have to consider all minimal (P,Q,R)-chains.
By using the rule removal processor [15] with the following polynomial ordering [25], at least one Dependency Pair or term rewrite system rule of this QDP problem can be strictly oriented.
Strictly oriented dependency pairs:

new_primModNatS(Succ(Succ(wv3000)), Zero) → new_primModNatS(new_primMinusNatS0(wv3000), Zero)

Strictly oriented rules of the TRS R:

new_primMinusNatS0(wv3000) → Succ(wv3000)

Used ordering: POLO with Polynomial interpretation [25]:

POL(Succ(x₁)) = 1 + 2·x₁
POL(Zero) = 0
POL(new_primMinusNatS0(x₁)) = 2 + 2·x₁
POL(new_primModNatS(x₁, x₂)) = x₁ + x₂

↳ HASKELL

  ↳ IFR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ Narrow

                ↳ AND

                  ↳ QDP

                  ↳ QDP

                    ↳ DependencyGraphProof

                      ↳ AND

                        ↳ QDP

                          ↳ UsableRulesProof

                            ↳ QDP

                              ↳ QReductionProof

                                ↳ QDP

                                  ↳ RuleRemovalProof

                                    ↳ QDP

                                      ↳ PisEmptyProof

                        ↳ QDP

                  ↳ QDP

Q DP problem:
P is empty.
R is empty.
The set Q consists of the following terms:

new_primMinusNatS0(x0)

We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.

↳ HASKELL

  ↳ IFR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ Narrow

                ↳ AND

                  ↳ QDP

                  ↳ QDP

                    ↳ DependencyGraphProof

                      ↳ AND

                        ↳ QDP

                        ↳ QDP

                          ↳ UsableRulesProof

                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primModNatS0(wv51, wv52, Succ(wv530), Zero) → new_primModNatS(new_primMinusNatS2(wv51, wv52), Succ(wv52))
new_primModNatS00(wv51, wv52) → new_primModNatS(new_primMinusNatS2(wv51, wv52), Succ(wv52))
new_primModNatS(Succ(Succ(wv3000)), Succ(wv4000)) → new_primModNatS0(wv3000, wv4000, wv3000, wv4000)
new_primModNatS0(wv51, wv52, Succ(wv530), Succ(wv540)) → new_primModNatS0(wv51, wv52, wv530, wv540)
new_primModNatS0(wv51, wv52, Zero, Zero) → new_primModNatS00(wv51, wv52)

The TRS R consists of the following rules:

new_primMinusNatS3(Zero, Succ(wv520)) → Zero
new_primMinusNatS3(Succ(wv510), Succ(wv520)) → new_primMinusNatS3(wv510, wv520)
new_primMinusNatS1 → Zero
new_primMinusNatS2(wv51, wv52) → new_primMinusNatS3(wv51, wv52)
new_primMinusNatS3(Zero, Zero) → Zero
new_primMinusNatS0(wv3000) → Succ(wv3000)
new_primMinusNatS3(Succ(wv510), Zero) → Succ(wv510)

The set Q consists of the following terms:

new_primMinusNatS3(Zero, Zero)
new_primMinusNatS3(Succ(x0), Zero)
new_primMinusNatS0(x0)
new_primMinusNatS2(x0, x1)
new_primMinusNatS3(Succ(x0), Succ(x1))
new_primMinusNatS1
new_primMinusNatS3(Zero, Succ(x0))

↳ HASKELL

  ↳ IFR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ Narrow

                ↳ AND

                  ↳ QDP

                  ↳ QDP

                    ↳ DependencyGraphProof

                      ↳ AND

                        ↳ QDP

                        ↳ QDP

                          ↳ UsableRulesProof

                            ↳ QDP

                              ↳ QReductionProof

                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primModNatS0(wv51, wv52, Succ(wv530), Zero) → new_primModNatS(new_primMinusNatS2(wv51, wv52), Succ(wv52))
new_primModNatS00(wv51, wv52) → new_primModNatS(new_primMinusNatS2(wv51, wv52), Succ(wv52))
new_primModNatS(Succ(Succ(wv3000)), Succ(wv4000)) → new_primModNatS0(wv3000, wv4000, wv3000, wv4000)
new_primModNatS0(wv51, wv52, Succ(wv530), Succ(wv540)) → new_primModNatS0(wv51, wv52, wv530, wv540)
new_primModNatS0(wv51, wv52, Zero, Zero) → new_primModNatS00(wv51, wv52)

The TRS R consists of the following rules:

new_primMinusNatS2(wv51, wv52) → new_primMinusNatS3(wv51, wv52)
new_primMinusNatS3(Zero, Succ(wv520)) → Zero
new_primMinusNatS3(Succ(wv510), Succ(wv520)) → new_primMinusNatS3(wv510, wv520)
new_primMinusNatS3(Zero, Zero) → Zero
new_primMinusNatS3(Succ(wv510), Zero) → Succ(wv510)

The set Q consists of the following terms:

new_primMinusNatS3(Zero, Zero)
new_primMinusNatS3(Succ(x0), Zero)
new_primMinusNatS0(x0)
new_primMinusNatS2(x0, x1)
new_primMinusNatS3(Succ(x0), Succ(x1))
new_primMinusNatS1
new_primMinusNatS3(Zero, Succ(x0))

We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.

new_primMinusNatS0(x0)
new_primMinusNatS1

↳ HASKELL

  ↳ IFR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ Narrow

                ↳ AND

                  ↳ QDP

                  ↳ QDP

                    ↳ DependencyGraphProof

                      ↳ AND

                        ↳ QDP

                        ↳ QDP

                          ↳ UsableRulesProof

                            ↳ QDP

                              ↳ QReductionProof

                                ↳ QDP

                                  ↳ Rewriting

                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primModNatS0(wv51, wv52, Succ(wv530), Zero) → new_primModNatS(new_primMinusNatS2(wv51, wv52), Succ(wv52))
new_primModNatS00(wv51, wv52) → new_primModNatS(new_primMinusNatS2(wv51, wv52), Succ(wv52))
new_primModNatS(Succ(Succ(wv3000)), Succ(wv4000)) → new_primModNatS0(wv3000, wv4000, wv3000, wv4000)
new_primModNatS0(wv51, wv52, Zero, Zero) → new_primModNatS00(wv51, wv52)
new_primModNatS0(wv51, wv52, Succ(wv530), Succ(wv540)) → new_primModNatS0(wv51, wv52, wv530, wv540)

The TRS R consists of the following rules:

new_primMinusNatS2(wv51, wv52) → new_primMinusNatS3(wv51, wv52)
new_primMinusNatS3(Zero, Succ(wv520)) → Zero
new_primMinusNatS3(Succ(wv510), Succ(wv520)) → new_primMinusNatS3(wv510, wv520)
new_primMinusNatS3(Zero, Zero) → Zero
new_primMinusNatS3(Succ(wv510), Zero) → Succ(wv510)

The set Q consists of the following terms:

new_primMinusNatS3(Zero, Zero)
new_primMinusNatS3(Succ(x0), Zero)
new_primMinusNatS2(x0, x1)
new_primMinusNatS3(Succ(x0), Succ(x1))
new_primMinusNatS3(Zero, Succ(x0))

We have to consider all minimal (P,Q,R)-chains.
By rewriting [15] the rule new_primModNatS0(wv51, wv52, Succ(wv530), Zero) → new_primModNatS(new_primMinusNatS2(wv51, wv52), Succ(wv52)) at position [0] we obtained the following new rules:

new_primModNatS0(wv51, wv52, Succ(wv530), Zero) → new_primModNatS(new_primMinusNatS3(wv51, wv52), Succ(wv52))

↳ HASKELL

  ↳ IFR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ Narrow

                ↳ AND

                  ↳ QDP

                  ↳ QDP

                    ↳ DependencyGraphProof

                      ↳ AND

                        ↳ QDP

                        ↳ QDP

                          ↳ UsableRulesProof

                            ↳ QDP

                              ↳ QReductionProof

                                ↳ QDP

                                  ↳ Rewriting

                                    ↳ QDP

                                      ↳ Rewriting

                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primModNatS00(wv51, wv52) → new_primModNatS(new_primMinusNatS2(wv51, wv52), Succ(wv52))
new_primModNatS0(wv51, wv52, Succ(wv530), Zero) → new_primModNatS(new_primMinusNatS3(wv51, wv52), Succ(wv52))
new_primModNatS(Succ(Succ(wv3000)), Succ(wv4000)) → new_primModNatS0(wv3000, wv4000, wv3000, wv4000)
new_primModNatS0(wv51, wv52, Succ(wv530), Succ(wv540)) → new_primModNatS0(wv51, wv52, wv530, wv540)
new_primModNatS0(wv51, wv52, Zero, Zero) → new_primModNatS00(wv51, wv52)

The TRS R consists of the following rules:

new_primMinusNatS2(wv51, wv52) → new_primMinusNatS3(wv51, wv52)
new_primMinusNatS3(Zero, Succ(wv520)) → Zero
new_primMinusNatS3(Succ(wv510), Succ(wv520)) → new_primMinusNatS3(wv510, wv520)
new_primMinusNatS3(Zero, Zero) → Zero
new_primMinusNatS3(Succ(wv510), Zero) → Succ(wv510)

The set Q consists of the following terms:

new_primMinusNatS3(Zero, Zero)
new_primMinusNatS3(Succ(x0), Zero)
new_primMinusNatS2(x0, x1)
new_primMinusNatS3(Succ(x0), Succ(x1))
new_primMinusNatS3(Zero, Succ(x0))

We have to consider all minimal (P,Q,R)-chains.
By rewriting [15] the rule new_primModNatS00(wv51, wv52) → new_primModNatS(new_primMinusNatS2(wv51, wv52), Succ(wv52)) at position [0] we obtained the following new rules:

new_primModNatS00(wv51, wv52) → new_primModNatS(new_primMinusNatS3(wv51, wv52), Succ(wv52))

↳ HASKELL

  ↳ IFR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ Narrow

                ↳ AND

                  ↳ QDP

                  ↳ QDP

                    ↳ DependencyGraphProof

                      ↳ AND

                        ↳ QDP

                        ↳ QDP

                          ↳ UsableRulesProof

                            ↳ QDP

                              ↳ QReductionProof

                                ↳ QDP

                                  ↳ Rewriting

                                    ↳ QDP

                                      ↳ Rewriting

                                        ↳ QDP

                                          ↳ UsableRulesProof

                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primModNatS0(wv51, wv52, Succ(wv530), Zero) → new_primModNatS(new_primMinusNatS3(wv51, wv52), Succ(wv52))
new_primModNatS(Succ(Succ(wv3000)), Succ(wv4000)) → new_primModNatS0(wv3000, wv4000, wv3000, wv4000)
new_primModNatS00(wv51, wv52) → new_primModNatS(new_primMinusNatS3(wv51, wv52), Succ(wv52))
new_primModNatS0(wv51, wv52, Zero, Zero) → new_primModNatS00(wv51, wv52)
new_primModNatS0(wv51, wv52, Succ(wv530), Succ(wv540)) → new_primModNatS0(wv51, wv52, wv530, wv540)

The TRS R consists of the following rules:

new_primMinusNatS2(wv51, wv52) → new_primMinusNatS3(wv51, wv52)
new_primMinusNatS3(Zero, Succ(wv520)) → Zero
new_primMinusNatS3(Succ(wv510), Succ(wv520)) → new_primMinusNatS3(wv510, wv520)
new_primMinusNatS3(Zero, Zero) → Zero
new_primMinusNatS3(Succ(wv510), Zero) → Succ(wv510)

The set Q consists of the following terms:

new_primMinusNatS3(Zero, Zero)
new_primMinusNatS3(Succ(x0), Zero)
new_primMinusNatS2(x0, x1)
new_primMinusNatS3(Succ(x0), Succ(x1))
new_primMinusNatS3(Zero, Succ(x0))

↳ HASKELL

  ↳ IFR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ Narrow

                ↳ AND

                  ↳ QDP

                  ↳ QDP

                    ↳ DependencyGraphProof

                      ↳ AND

                        ↳ QDP

                        ↳ QDP

                          ↳ UsableRulesProof

                            ↳ QDP

                              ↳ QReductionProof

                                ↳ QDP

                                  ↳ Rewriting

                                    ↳ QDP

                                      ↳ Rewriting

                                        ↳ QDP

                                          ↳ UsableRulesProof

                                            ↳ QDP

                                              ↳ QReductionProof

                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primModNatS0(wv51, wv52, Succ(wv530), Zero) → new_primModNatS(new_primMinusNatS3(wv51, wv52), Succ(wv52))
new_primModNatS(Succ(Succ(wv3000)), Succ(wv4000)) → new_primModNatS0(wv3000, wv4000, wv3000, wv4000)
new_primModNatS00(wv51, wv52) → new_primModNatS(new_primMinusNatS3(wv51, wv52), Succ(wv52))
new_primModNatS0(wv51, wv52, Zero, Zero) → new_primModNatS00(wv51, wv52)
new_primModNatS0(wv51, wv52, Succ(wv530), Succ(wv540)) → new_primModNatS0(wv51, wv52, wv530, wv540)

The TRS R consists of the following rules:

new_primMinusNatS3(Zero, Succ(wv520)) → Zero
new_primMinusNatS3(Succ(wv510), Succ(wv520)) → new_primMinusNatS3(wv510, wv520)
new_primMinusNatS3(Zero, Zero) → Zero
new_primMinusNatS3(Succ(wv510), Zero) → Succ(wv510)

The set Q consists of the following terms:

new_primMinusNatS3(Zero, Zero)
new_primMinusNatS3(Succ(x0), Zero)
new_primMinusNatS2(x0, x1)
new_primMinusNatS3(Succ(x0), Succ(x1))
new_primMinusNatS3(Zero, Succ(x0))

We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.

new_primMinusNatS2(x0, x1)

↳ HASKELL

  ↳ IFR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ Narrow

                ↳ AND

                  ↳ QDP

                  ↳ QDP

                    ↳ DependencyGraphProof

                      ↳ AND

                        ↳ QDP

                        ↳ QDP

                          ↳ UsableRulesProof

                            ↳ QDP

                              ↳ QReductionProof

                                ↳ QDP

                                  ↳ Rewriting

                                    ↳ QDP

                                      ↳ Rewriting

                                        ↳ QDP

                                          ↳ UsableRulesProof

                                            ↳ QDP

                                              ↳ QReductionProof

                                                ↳ QDP

                                                  ↳ QDPOrderProof

                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primModNatS0(wv51, wv52, Succ(wv530), Zero) → new_primModNatS(new_primMinusNatS3(wv51, wv52), Succ(wv52))
new_primModNatS(Succ(Succ(wv3000)), Succ(wv4000)) → new_primModNatS0(wv3000, wv4000, wv3000, wv4000)
new_primModNatS00(wv51, wv52) → new_primModNatS(new_primMinusNatS3(wv51, wv52), Succ(wv52))
new_primModNatS0(wv51, wv52, Succ(wv530), Succ(wv540)) → new_primModNatS0(wv51, wv52, wv530, wv540)
new_primModNatS0(wv51, wv52, Zero, Zero) → new_primModNatS00(wv51, wv52)

The TRS R consists of the following rules:

new_primMinusNatS3(Zero, Succ(wv520)) → Zero
new_primMinusNatS3(Succ(wv510), Succ(wv520)) → new_primMinusNatS3(wv510, wv520)
new_primMinusNatS3(Zero, Zero) → Zero
new_primMinusNatS3(Succ(wv510), Zero) → Succ(wv510)

The set Q consists of the following terms:

new_primMinusNatS3(Zero, Zero)
new_primMinusNatS3(Succ(x0), Zero)
new_primMinusNatS3(Succ(x0), Succ(x1))
new_primMinusNatS3(Zero, Succ(x0))

We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [15].

The following pairs can be oriented strictly and are deleted.

new_primModNatS(Succ(Succ(wv3000)), Succ(wv4000)) → new_primModNatS0(wv3000, wv4000, wv3000, wv4000)

The remaining pairs can at least be oriented weakly.

new_primModNatS0(wv51, wv52, Succ(wv530), Zero) → new_primModNatS(new_primMinusNatS3(wv51, wv52), Succ(wv52))
new_primModNatS00(wv51, wv52) → new_primModNatS(new_primMinusNatS3(wv51, wv52), Succ(wv52))
new_primModNatS0(wv51, wv52, Succ(wv530), Succ(wv540)) → new_primModNatS0(wv51, wv52, wv530, wv540)
new_primModNatS0(wv51, wv52, Zero, Zero) → new_primModNatS00(wv51, wv52)

Used ordering: Polynomial interpretation [25]:

POL(Succ(x₁)) = 1 + x₁
POL(Zero) = 0
POL(new_primMinusNatS3(x₁, x₂)) = x₁
POL(new_primModNatS(x₁, x₂)) = x₁
POL(new_primModNatS0(x₁, x₂, x₃, x₄)) = x₁
POL(new_primModNatS00(x₁, x₂)) = x₁

The following usable rules [17] were oriented:

new_primMinusNatS3(Zero, Zero) → Zero
new_primMinusNatS3(Zero, Succ(wv520)) → Zero
new_primMinusNatS3(Succ(wv510), Zero) → Succ(wv510)
new_primMinusNatS3(Succ(wv510), Succ(wv520)) → new_primMinusNatS3(wv510, wv520)

↳ HASKELL

  ↳ IFR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ Narrow

                ↳ AND

                  ↳ QDP

                  ↳ QDP

                    ↳ DependencyGraphProof

                      ↳ AND

                        ↳ QDP

                        ↳ QDP

                          ↳ UsableRulesProof

                            ↳ QDP

                              ↳ QReductionProof

                                ↳ QDP

                                  ↳ Rewriting

                                    ↳ QDP

                                      ↳ Rewriting

                                        ↳ QDP

                                          ↳ UsableRulesProof

                                            ↳ QDP

                                              ↳ QReductionProof

                                                ↳ QDP

                                                  ↳ QDPOrderProof

                                                    ↳ QDP

                                                      ↳ DependencyGraphProof

                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primModNatS0(wv51, wv52, Succ(wv530), Zero) → new_primModNatS(new_primMinusNatS3(wv51, wv52), Succ(wv52))
new_primModNatS00(wv51, wv52) → new_primModNatS(new_primMinusNatS3(wv51, wv52), Succ(wv52))
new_primModNatS0(wv51, wv52, Zero, Zero) → new_primModNatS00(wv51, wv52)
new_primModNatS0(wv51, wv52, Succ(wv530), Succ(wv540)) → new_primModNatS0(wv51, wv52, wv530, wv540)

The TRS R consists of the following rules:

new_primMinusNatS3(Zero, Succ(wv520)) → Zero
new_primMinusNatS3(Succ(wv510), Succ(wv520)) → new_primMinusNatS3(wv510, wv520)
new_primMinusNatS3(Zero, Zero) → Zero
new_primMinusNatS3(Succ(wv510), Zero) → Succ(wv510)

The set Q consists of the following terms:

new_primMinusNatS3(Zero, Zero)
new_primMinusNatS3(Succ(x0), Zero)
new_primMinusNatS3(Succ(x0), Succ(x1))
new_primMinusNatS3(Zero, Succ(x0))

We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 1 SCC with 3 less nodes.

↳ HASKELL

  ↳ IFR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ Narrow

                ↳ AND

                  ↳ QDP

                  ↳ QDP

                    ↳ DependencyGraphProof

                      ↳ AND

                        ↳ QDP

                        ↳ QDP

                          ↳ UsableRulesProof

                            ↳ QDP

                              ↳ QReductionProof

                                ↳ QDP

                                  ↳ Rewriting

                                    ↳ QDP

                                      ↳ Rewriting

                                        ↳ QDP

                                          ↳ UsableRulesProof

                                            ↳ QDP

                                              ↳ QReductionProof

                                                ↳ QDP

                                                  ↳ QDPOrderProof

                                                    ↳ QDP

                                                      ↳ DependencyGraphProof

                                                        ↳ QDP

                                                          ↳ UsableRulesProof

                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primModNatS0(wv51, wv52, Succ(wv530), Succ(wv540)) → new_primModNatS0(wv51, wv52, wv530, wv540)

The TRS R consists of the following rules:

new_primMinusNatS3(Zero, Succ(wv520)) → Zero
new_primMinusNatS3(Succ(wv510), Succ(wv520)) → new_primMinusNatS3(wv510, wv520)
new_primMinusNatS3(Zero, Zero) → Zero
new_primMinusNatS3(Succ(wv510), Zero) → Succ(wv510)

The set Q consists of the following terms:

new_primMinusNatS3(Zero, Zero)
new_primMinusNatS3(Succ(x0), Zero)
new_primMinusNatS3(Succ(x0), Succ(x1))
new_primMinusNatS3(Zero, Succ(x0))

↳ HASKELL

  ↳ IFR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ Narrow

                ↳ AND

                  ↳ QDP

                  ↳ QDP

                    ↳ DependencyGraphProof

                      ↳ AND

                        ↳ QDP

                        ↳ QDP

                          ↳ UsableRulesProof

                            ↳ QDP

                              ↳ QReductionProof

                                ↳ QDP

                                  ↳ Rewriting

                                    ↳ QDP

                                      ↳ Rewriting

                                        ↳ QDP

                                          ↳ UsableRulesProof

                                            ↳ QDP

                                              ↳ QReductionProof

                                                ↳ QDP

                                                  ↳ QDPOrderProof

                                                    ↳ QDP

                                                      ↳ DependencyGraphProof

                                                        ↳ QDP

                                                          ↳ UsableRulesProof

                                                            ↳ QDP

                                                              ↳ QReductionProof

                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primModNatS0(wv51, wv52, Succ(wv530), Succ(wv540)) → new_primModNatS0(wv51, wv52, wv530, wv540)

R is empty.
The set Q consists of the following terms:

new_primMinusNatS3(Zero, Zero)
new_primMinusNatS3(Succ(x0), Zero)
new_primMinusNatS3(Succ(x0), Succ(x1))
new_primMinusNatS3(Zero, Succ(x0))

We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.

new_primMinusNatS3(Zero, Zero)
new_primMinusNatS3(Succ(x0), Zero)
new_primMinusNatS3(Succ(x0), Succ(x1))
new_primMinusNatS3(Zero, Succ(x0))

↳ HASKELL

  ↳ IFR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ Narrow

                ↳ AND

                  ↳ QDP

                  ↳ QDP

                    ↳ DependencyGraphProof

                      ↳ AND

                        ↳ QDP

                        ↳ QDP

                          ↳ UsableRulesProof

                            ↳ QDP

                              ↳ QReductionProof

                                ↳ QDP

                                  ↳ Rewriting

                                    ↳ QDP

                                      ↳ Rewriting

                                        ↳ QDP

                                          ↳ UsableRulesProof

                                            ↳ QDP

                                              ↳ QReductionProof

                                                ↳ QDP

                                                  ↳ QDPOrderProof

                                                    ↳ QDP

                                                      ↳ DependencyGraphProof

                                                        ↳ QDP

                                                          ↳ UsableRulesProof

                                                            ↳ QDP

                                                              ↳ QReductionProof

                                                                ↳ QDP

                                                                  ↳ QDPSizeChangeProof

                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primModNatS0(wv51, wv52, Succ(wv530), Succ(wv540)) → new_primModNatS0(wv51, wv52, wv530, wv540)

From the DPs we obtained the following set of size-change graphs:

new_primModNatS0(wv51, wv52, Succ(wv530), Succ(wv540)) → new_primModNatS0(wv51, wv52, wv530, wv540)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 > 3, 4 > 4

↳ HASKELL

  ↳ IFR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ Narrow

                ↳ AND

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                    ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

new_primDivNatS0(wv46, wv47, Zero, Zero) → new_primDivNatS00(wv46, wv47)
new_primDivNatS0(wv46, wv47, Succ(wv480), Succ(wv490)) → new_primDivNatS0(wv46, wv47, wv480, wv490)
new_primDivNatS0(wv46, wv47, Succ(wv480), Zero) → new_primDivNatS(new_primMinusNatS2(wv46, wv47), Succ(wv47))
new_primDivNatS(Succ(Succ(wv3000)), Succ(wv4000)) → new_primDivNatS0(wv3000, wv4000, wv3000, wv4000)
new_primDivNatS00(wv46, wv47) → new_primDivNatS(new_primMinusNatS2(wv46, wv47), Succ(wv47))
new_primDivNatS(Succ(Succ(wv3000)), Zero) → new_primDivNatS(new_primMinusNatS0(wv3000), Zero)
new_primDivNatS(Succ(Zero), Zero) → new_primDivNatS(new_primMinusNatS1, Zero)

The TRS R consists of the following rules:

new_primMinusNatS3(Zero, Succ(wv520)) → Zero
new_primMinusNatS3(Succ(wv510), Succ(wv520)) → new_primMinusNatS3(wv510, wv520)
new_primMinusNatS1 → Zero
new_primMinusNatS2(wv51, wv52) → new_primMinusNatS3(wv51, wv52)
new_primMinusNatS3(Zero, Zero) → Zero
new_primMinusNatS0(wv3000) → Succ(wv3000)
new_primMinusNatS3(Succ(wv510), Zero) → Succ(wv510)

The set Q consists of the following terms:

new_primMinusNatS3(Zero, Zero)
new_primMinusNatS3(Succ(x0), Zero)
new_primMinusNatS0(x0)
new_primMinusNatS2(x0, x1)
new_primMinusNatS3(Succ(x0), Succ(x1))
new_primMinusNatS1
new_primMinusNatS3(Zero, Succ(x0))

We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 2 SCCs with 1 less node.

↳ HASKELL

  ↳ IFR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ Narrow

                ↳ AND

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                    ↳ DependencyGraphProof

                      ↳ AND

                        ↳ QDP

                          ↳ UsableRulesProof

                        ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primDivNatS(Succ(Succ(wv3000)), Zero) → new_primDivNatS(new_primMinusNatS0(wv3000), Zero)

The TRS R consists of the following rules:

new_primMinusNatS3(Zero, Succ(wv520)) → Zero
new_primMinusNatS3(Succ(wv510), Succ(wv520)) → new_primMinusNatS3(wv510, wv520)
new_primMinusNatS1 → Zero
new_primMinusNatS2(wv51, wv52) → new_primMinusNatS3(wv51, wv52)
new_primMinusNatS3(Zero, Zero) → Zero
new_primMinusNatS0(wv3000) → Succ(wv3000)
new_primMinusNatS3(Succ(wv510), Zero) → Succ(wv510)

The set Q consists of the following terms:

new_primMinusNatS3(Zero, Zero)
new_primMinusNatS3(Succ(x0), Zero)
new_primMinusNatS0(x0)
new_primMinusNatS2(x0, x1)
new_primMinusNatS3(Succ(x0), Succ(x1))
new_primMinusNatS1
new_primMinusNatS3(Zero, Succ(x0))

↳ HASKELL

  ↳ IFR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ Narrow

                ↳ AND

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                    ↳ DependencyGraphProof

                      ↳ AND

                        ↳ QDP

                          ↳ UsableRulesProof

                            ↳ QDP

                              ↳ QReductionProof

                        ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primDivNatS(Succ(Succ(wv3000)), Zero) → new_primDivNatS(new_primMinusNatS0(wv3000), Zero)

The TRS R consists of the following rules:

new_primMinusNatS0(wv3000) → Succ(wv3000)

The set Q consists of the following terms:

new_primMinusNatS3(Zero, Zero)
new_primMinusNatS3(Succ(x0), Zero)
new_primMinusNatS0(x0)
new_primMinusNatS2(x0, x1)
new_primMinusNatS3(Succ(x0), Succ(x1))
new_primMinusNatS1
new_primMinusNatS3(Zero, Succ(x0))

We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.

new_primMinusNatS3(Zero, Zero)
new_primMinusNatS3(Succ(x0), Zero)
new_primMinusNatS2(x0, x1)
new_primMinusNatS3(Succ(x0), Succ(x1))
new_primMinusNatS1
new_primMinusNatS3(Zero, Succ(x0))

↳ HASKELL

  ↳ IFR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ Narrow

                ↳ AND

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                    ↳ DependencyGraphProof

                      ↳ AND

                        ↳ QDP

                          ↳ UsableRulesProof

                            ↳ QDP

                              ↳ QReductionProof

                                ↳ QDP

                                  ↳ RuleRemovalProof

                        ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primDivNatS(Succ(Succ(wv3000)), Zero) → new_primDivNatS(new_primMinusNatS0(wv3000), Zero)

The TRS R consists of the following rules:

new_primMinusNatS0(wv3000) → Succ(wv3000)

The set Q consists of the following terms:

new_primMinusNatS0(x0)

new_primDivNatS(Succ(Succ(wv3000)), Zero) → new_primDivNatS(new_primMinusNatS0(wv3000), Zero)

Strictly oriented rules of the TRS R:

new_primMinusNatS0(wv3000) → Succ(wv3000)

Used ordering: POLO with Polynomial interpretation [25]:

POL(Succ(x₁)) = 1 + 2·x₁
POL(Zero) = 0
POL(new_primDivNatS(x₁, x₂)) = x₁ + x₂
POL(new_primMinusNatS0(x₁)) = 2 + 2·x₁

↳ HASKELL

  ↳ IFR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ Narrow

                ↳ AND

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                    ↳ DependencyGraphProof

                      ↳ AND

                        ↳ QDP

                          ↳ UsableRulesProof

                            ↳ QDP

                              ↳ QReductionProof

                                ↳ QDP

                                  ↳ RuleRemovalProof

                                    ↳ QDP

                                      ↳ PisEmptyProof

                        ↳ QDP

Q DP problem:
P is empty.
R is empty.
The set Q consists of the following terms:

new_primMinusNatS0(x0)

We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.

↳ HASKELL

  ↳ IFR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ Narrow

                ↳ AND

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                    ↳ DependencyGraphProof

                      ↳ AND

                        ↳ QDP

                        ↳ QDP

                          ↳ UsableRulesProof

Q DP problem:
The TRS P consists of the following rules:

new_primDivNatS0(wv46, wv47, Zero, Zero) → new_primDivNatS00(wv46, wv47)
new_primDivNatS0(wv46, wv47, Succ(wv480), Succ(wv490)) → new_primDivNatS0(wv46, wv47, wv480, wv490)
new_primDivNatS0(wv46, wv47, Succ(wv480), Zero) → new_primDivNatS(new_primMinusNatS2(wv46, wv47), Succ(wv47))
new_primDivNatS(Succ(Succ(wv3000)), Succ(wv4000)) → new_primDivNatS0(wv3000, wv4000, wv3000, wv4000)
new_primDivNatS00(wv46, wv47) → new_primDivNatS(new_primMinusNatS2(wv46, wv47), Succ(wv47))

The TRS R consists of the following rules:

new_primMinusNatS3(Zero, Succ(wv520)) → Zero
new_primMinusNatS3(Succ(wv510), Succ(wv520)) → new_primMinusNatS3(wv510, wv520)
new_primMinusNatS1 → Zero
new_primMinusNatS2(wv51, wv52) → new_primMinusNatS3(wv51, wv52)
new_primMinusNatS3(Zero, Zero) → Zero
new_primMinusNatS0(wv3000) → Succ(wv3000)
new_primMinusNatS3(Succ(wv510), Zero) → Succ(wv510)

The set Q consists of the following terms:

new_primMinusNatS3(Zero, Zero)
new_primMinusNatS3(Succ(x0), Zero)
new_primMinusNatS0(x0)
new_primMinusNatS2(x0, x1)
new_primMinusNatS3(Succ(x0), Succ(x1))
new_primMinusNatS1
new_primMinusNatS3(Zero, Succ(x0))

↳ HASKELL

  ↳ IFR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ Narrow

                ↳ AND

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                    ↳ DependencyGraphProof

                      ↳ AND

                        ↳ QDP

                        ↳ QDP

                          ↳ UsableRulesProof

                            ↳ QDP

                              ↳ QReductionProof

Q DP problem:
The TRS P consists of the following rules:

new_primDivNatS0(wv46, wv47, Zero, Zero) → new_primDivNatS00(wv46, wv47)
new_primDivNatS0(wv46, wv47, Succ(wv480), Succ(wv490)) → new_primDivNatS0(wv46, wv47, wv480, wv490)
new_primDivNatS0(wv46, wv47, Succ(wv480), Zero) → new_primDivNatS(new_primMinusNatS2(wv46, wv47), Succ(wv47))
new_primDivNatS(Succ(Succ(wv3000)), Succ(wv4000)) → new_primDivNatS0(wv3000, wv4000, wv3000, wv4000)
new_primDivNatS00(wv46, wv47) → new_primDivNatS(new_primMinusNatS2(wv46, wv47), Succ(wv47))

The TRS R consists of the following rules:

new_primMinusNatS2(wv51, wv52) → new_primMinusNatS3(wv51, wv52)
new_primMinusNatS3(Zero, Succ(wv520)) → Zero
new_primMinusNatS3(Succ(wv510), Succ(wv520)) → new_primMinusNatS3(wv510, wv520)
new_primMinusNatS3(Zero, Zero) → Zero
new_primMinusNatS3(Succ(wv510), Zero) → Succ(wv510)

The set Q consists of the following terms:

new_primMinusNatS3(Zero, Zero)
new_primMinusNatS3(Succ(x0), Zero)
new_primMinusNatS0(x0)
new_primMinusNatS2(x0, x1)
new_primMinusNatS3(Succ(x0), Succ(x1))
new_primMinusNatS1
new_primMinusNatS3(Zero, Succ(x0))

We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.

new_primMinusNatS0(x0)
new_primMinusNatS1

↳ HASKELL

  ↳ IFR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ Narrow

                ↳ AND

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                    ↳ DependencyGraphProof

                      ↳ AND

                        ↳ QDP

                        ↳ QDP

                          ↳ UsableRulesProof

                            ↳ QDP

                              ↳ QReductionProof

                                ↳ QDP

                                  ↳ Rewriting

Q DP problem:
The TRS P consists of the following rules:

new_primDivNatS0(wv46, wv47, Zero, Zero) → new_primDivNatS00(wv46, wv47)
new_primDivNatS(Succ(Succ(wv3000)), Succ(wv4000)) → new_primDivNatS0(wv3000, wv4000, wv3000, wv4000)
new_primDivNatS0(wv46, wv47, Succ(wv480), Zero) → new_primDivNatS(new_primMinusNatS2(wv46, wv47), Succ(wv47))
new_primDivNatS0(wv46, wv47, Succ(wv480), Succ(wv490)) → new_primDivNatS0(wv46, wv47, wv480, wv490)
new_primDivNatS00(wv46, wv47) → new_primDivNatS(new_primMinusNatS2(wv46, wv47), Succ(wv47))

The TRS R consists of the following rules:

new_primMinusNatS2(wv51, wv52) → new_primMinusNatS3(wv51, wv52)
new_primMinusNatS3(Zero, Succ(wv520)) → Zero
new_primMinusNatS3(Succ(wv510), Succ(wv520)) → new_primMinusNatS3(wv510, wv520)
new_primMinusNatS3(Zero, Zero) → Zero
new_primMinusNatS3(Succ(wv510), Zero) → Succ(wv510)

The set Q consists of the following terms:

new_primMinusNatS3(Zero, Zero)
new_primMinusNatS3(Succ(x0), Zero)
new_primMinusNatS2(x0, x1)
new_primMinusNatS3(Succ(x0), Succ(x1))
new_primMinusNatS3(Zero, Succ(x0))

We have to consider all minimal (P,Q,R)-chains.
By rewriting [15] the rule new_primDivNatS0(wv46, wv47, Succ(wv480), Zero) → new_primDivNatS(new_primMinusNatS2(wv46, wv47), Succ(wv47)) at position [0] we obtained the following new rules:

new_primDivNatS0(wv46, wv47, Succ(wv480), Zero) → new_primDivNatS(new_primMinusNatS3(wv46, wv47), Succ(wv47))

↳ HASKELL

  ↳ IFR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ Narrow

                ↳ AND

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                    ↳ DependencyGraphProof

                      ↳ AND

                        ↳ QDP

                        ↳ QDP

                          ↳ UsableRulesProof

                            ↳ QDP

                              ↳ QReductionProof

                                ↳ QDP

                                  ↳ Rewriting

                                    ↳ QDP

                                      ↳ Rewriting

Q DP problem:
The TRS P consists of the following rules:

new_primDivNatS0(wv46, wv47, Zero, Zero) → new_primDivNatS00(wv46, wv47)
new_primDivNatS0(wv46, wv47, Succ(wv480), Succ(wv490)) → new_primDivNatS0(wv46, wv47, wv480, wv490)
new_primDivNatS(Succ(Succ(wv3000)), Succ(wv4000)) → new_primDivNatS0(wv3000, wv4000, wv3000, wv4000)
new_primDivNatS00(wv46, wv47) → new_primDivNatS(new_primMinusNatS2(wv46, wv47), Succ(wv47))
new_primDivNatS0(wv46, wv47, Succ(wv480), Zero) → new_primDivNatS(new_primMinusNatS3(wv46, wv47), Succ(wv47))

The TRS R consists of the following rules:

new_primMinusNatS2(wv51, wv52) → new_primMinusNatS3(wv51, wv52)
new_primMinusNatS3(Zero, Succ(wv520)) → Zero
new_primMinusNatS3(Succ(wv510), Succ(wv520)) → new_primMinusNatS3(wv510, wv520)
new_primMinusNatS3(Zero, Zero) → Zero
new_primMinusNatS3(Succ(wv510), Zero) → Succ(wv510)

The set Q consists of the following terms:

new_primMinusNatS3(Zero, Zero)
new_primMinusNatS3(Succ(x0), Zero)
new_primMinusNatS2(x0, x1)
new_primMinusNatS3(Succ(x0), Succ(x1))
new_primMinusNatS3(Zero, Succ(x0))

We have to consider all minimal (P,Q,R)-chains.
By rewriting [15] the rule new_primDivNatS00(wv46, wv47) → new_primDivNatS(new_primMinusNatS2(wv46, wv47), Succ(wv47)) at position [0] we obtained the following new rules:

new_primDivNatS00(wv46, wv47) → new_primDivNatS(new_primMinusNatS3(wv46, wv47), Succ(wv47))

↳ HASKELL

  ↳ IFR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ Narrow

                ↳ AND

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                    ↳ DependencyGraphProof

                      ↳ AND

                        ↳ QDP

                        ↳ QDP

                          ↳ UsableRulesProof

                            ↳ QDP

                              ↳ QReductionProof

                                ↳ QDP

                                  ↳ Rewriting

                                    ↳ QDP

                                      ↳ Rewriting

                                        ↳ QDP

                                          ↳ UsableRulesProof

Q DP problem:
The TRS P consists of the following rules:

new_primDivNatS0(wv46, wv47, Zero, Zero) → new_primDivNatS00(wv46, wv47)
new_primDivNatS(Succ(Succ(wv3000)), Succ(wv4000)) → new_primDivNatS0(wv3000, wv4000, wv3000, wv4000)
new_primDivNatS0(wv46, wv47, Succ(wv480), Succ(wv490)) → new_primDivNatS0(wv46, wv47, wv480, wv490)
new_primDivNatS00(wv46, wv47) → new_primDivNatS(new_primMinusNatS3(wv46, wv47), Succ(wv47))
new_primDivNatS0(wv46, wv47, Succ(wv480), Zero) → new_primDivNatS(new_primMinusNatS3(wv46, wv47), Succ(wv47))

The TRS R consists of the following rules:

new_primMinusNatS2(wv51, wv52) → new_primMinusNatS3(wv51, wv52)
new_primMinusNatS3(Zero, Succ(wv520)) → Zero
new_primMinusNatS3(Succ(wv510), Succ(wv520)) → new_primMinusNatS3(wv510, wv520)
new_primMinusNatS3(Zero, Zero) → Zero
new_primMinusNatS3(Succ(wv510), Zero) → Succ(wv510)

The set Q consists of the following terms:

new_primMinusNatS3(Zero, Zero)
new_primMinusNatS3(Succ(x0), Zero)
new_primMinusNatS2(x0, x1)
new_primMinusNatS3(Succ(x0), Succ(x1))
new_primMinusNatS3(Zero, Succ(x0))

↳ HASKELL

  ↳ IFR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ Narrow

                ↳ AND

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                    ↳ DependencyGraphProof

                      ↳ AND

                        ↳ QDP

                        ↳ QDP

                          ↳ UsableRulesProof

                            ↳ QDP

                              ↳ QReductionProof

                                ↳ QDP

                                  ↳ Rewriting

                                    ↳ QDP

                                      ↳ Rewriting

                                        ↳ QDP

                                          ↳ UsableRulesProof

                                            ↳ QDP

                                              ↳ QReductionProof

Q DP problem:
The TRS P consists of the following rules:

new_primDivNatS0(wv46, wv47, Zero, Zero) → new_primDivNatS00(wv46, wv47)
new_primDivNatS(Succ(Succ(wv3000)), Succ(wv4000)) → new_primDivNatS0(wv3000, wv4000, wv3000, wv4000)
new_primDivNatS0(wv46, wv47, Succ(wv480), Succ(wv490)) → new_primDivNatS0(wv46, wv47, wv480, wv490)
new_primDivNatS00(wv46, wv47) → new_primDivNatS(new_primMinusNatS3(wv46, wv47), Succ(wv47))
new_primDivNatS0(wv46, wv47, Succ(wv480), Zero) → new_primDivNatS(new_primMinusNatS3(wv46, wv47), Succ(wv47))

The TRS R consists of the following rules:

new_primMinusNatS3(Zero, Succ(wv520)) → Zero
new_primMinusNatS3(Succ(wv510), Succ(wv520)) → new_primMinusNatS3(wv510, wv520)
new_primMinusNatS3(Zero, Zero) → Zero
new_primMinusNatS3(Succ(wv510), Zero) → Succ(wv510)

The set Q consists of the following terms:

new_primMinusNatS3(Zero, Zero)
new_primMinusNatS3(Succ(x0), Zero)
new_primMinusNatS2(x0, x1)
new_primMinusNatS3(Succ(x0), Succ(x1))
new_primMinusNatS3(Zero, Succ(x0))

We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.

new_primMinusNatS2(x0, x1)

↳ HASKELL

  ↳ IFR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ Narrow

                ↳ AND

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                    ↳ DependencyGraphProof

                      ↳ AND

                        ↳ QDP

                        ↳ QDP

                          ↳ UsableRulesProof

                            ↳ QDP

                              ↳ QReductionProof

                                ↳ QDP

                                  ↳ Rewriting

                                    ↳ QDP

                                      ↳ Rewriting

                                        ↳ QDP

                                          ↳ UsableRulesProof

                                            ↳ QDP

                                              ↳ QReductionProof

                                                ↳ QDP

                                                  ↳ QDPOrderProof

Q DP problem:
The TRS P consists of the following rules:

new_primDivNatS0(wv46, wv47, Zero, Zero) → new_primDivNatS00(wv46, wv47)
new_primDivNatS0(wv46, wv47, Succ(wv480), Succ(wv490)) → new_primDivNatS0(wv46, wv47, wv480, wv490)
new_primDivNatS(Succ(Succ(wv3000)), Succ(wv4000)) → new_primDivNatS0(wv3000, wv4000, wv3000, wv4000)
new_primDivNatS0(wv46, wv47, Succ(wv480), Zero) → new_primDivNatS(new_primMinusNatS3(wv46, wv47), Succ(wv47))
new_primDivNatS00(wv46, wv47) → new_primDivNatS(new_primMinusNatS3(wv46, wv47), Succ(wv47))

The TRS R consists of the following rules:

new_primMinusNatS3(Zero, Succ(wv520)) → Zero
new_primMinusNatS3(Succ(wv510), Succ(wv520)) → new_primMinusNatS3(wv510, wv520)
new_primMinusNatS3(Zero, Zero) → Zero
new_primMinusNatS3(Succ(wv510), Zero) → Succ(wv510)

The set Q consists of the following terms:

new_primMinusNatS3(Zero, Zero)
new_primMinusNatS3(Succ(x0), Zero)
new_primMinusNatS3(Succ(x0), Succ(x1))
new_primMinusNatS3(Zero, Succ(x0))

We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [15].

The following pairs can be oriented strictly and are deleted.

new_primDivNatS(Succ(Succ(wv3000)), Succ(wv4000)) → new_primDivNatS0(wv3000, wv4000, wv3000, wv4000)

The remaining pairs can at least be oriented weakly.

new_primDivNatS0(wv46, wv47, Zero, Zero) → new_primDivNatS00(wv46, wv47)
new_primDivNatS0(wv46, wv47, Succ(wv480), Succ(wv490)) → new_primDivNatS0(wv46, wv47, wv480, wv490)
new_primDivNatS0(wv46, wv47, Succ(wv480), Zero) → new_primDivNatS(new_primMinusNatS3(wv46, wv47), Succ(wv47))
new_primDivNatS00(wv46, wv47) → new_primDivNatS(new_primMinusNatS3(wv46, wv47), Succ(wv47))

Used ordering: Polynomial interpretation [25]:

POL(Succ(x₁)) = 1 + x₁
POL(Zero) = 0
POL(new_primDivNatS(x₁, x₂)) = x₁
POL(new_primDivNatS0(x₁, x₂, x₃, x₄)) = x₁
POL(new_primDivNatS00(x₁, x₂)) = x₁
POL(new_primMinusNatS3(x₁, x₂)) = x₁

The following usable rules [17] were oriented:

new_primMinusNatS3(Zero, Zero) → Zero
new_primMinusNatS3(Succ(wv510), Succ(wv520)) → new_primMinusNatS3(wv510, wv520)
new_primMinusNatS3(Succ(wv510), Zero) → Succ(wv510)
new_primMinusNatS3(Zero, Succ(wv520)) → Zero

↳ HASKELL

  ↳ IFR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ Narrow

                ↳ AND

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                    ↳ DependencyGraphProof

                      ↳ AND

                        ↳ QDP

                        ↳ QDP

                          ↳ UsableRulesProof

                            ↳ QDP

                              ↳ QReductionProof

                                ↳ QDP

                                  ↳ Rewriting

                                    ↳ QDP

                                      ↳ Rewriting

                                        ↳ QDP

                                          ↳ UsableRulesProof

                                            ↳ QDP

                                              ↳ QReductionProof

                                                ↳ QDP

                                                  ↳ QDPOrderProof

                                                    ↳ QDP

                                                      ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

new_primDivNatS0(wv46, wv47, Zero, Zero) → new_primDivNatS00(wv46, wv47)
new_primDivNatS0(wv46, wv47, Succ(wv480), Succ(wv490)) → new_primDivNatS0(wv46, wv47, wv480, wv490)
new_primDivNatS00(wv46, wv47) → new_primDivNatS(new_primMinusNatS3(wv46, wv47), Succ(wv47))
new_primDivNatS0(wv46, wv47, Succ(wv480), Zero) → new_primDivNatS(new_primMinusNatS3(wv46, wv47), Succ(wv47))

The TRS R consists of the following rules:

new_primMinusNatS3(Zero, Succ(wv520)) → Zero
new_primMinusNatS3(Succ(wv510), Succ(wv520)) → new_primMinusNatS3(wv510, wv520)
new_primMinusNatS3(Zero, Zero) → Zero
new_primMinusNatS3(Succ(wv510), Zero) → Succ(wv510)

The set Q consists of the following terms:

new_primMinusNatS3(Zero, Zero)
new_primMinusNatS3(Succ(x0), Zero)
new_primMinusNatS3(Succ(x0), Succ(x1))
new_primMinusNatS3(Zero, Succ(x0))

We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 1 SCC with 3 less nodes.

↳ HASKELL

  ↳ IFR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ Narrow

                ↳ AND

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                    ↳ DependencyGraphProof

                      ↳ AND

                        ↳ QDP

                        ↳ QDP

                          ↳ UsableRulesProof

                            ↳ QDP

                              ↳ QReductionProof

                                ↳ QDP

                                  ↳ Rewriting

                                    ↳ QDP

                                      ↳ Rewriting

                                        ↳ QDP

                                          ↳ UsableRulesProof

                                            ↳ QDP

                                              ↳ QReductionProof

                                                ↳ QDP

                                                  ↳ QDPOrderProof

                                                    ↳ QDP

                                                      ↳ DependencyGraphProof

                                                        ↳ QDP

                                                          ↳ UsableRulesProof

Q DP problem:
The TRS P consists of the following rules:

new_primDivNatS0(wv46, wv47, Succ(wv480), Succ(wv490)) → new_primDivNatS0(wv46, wv47, wv480, wv490)

The TRS R consists of the following rules:

new_primMinusNatS3(Zero, Succ(wv520)) → Zero
new_primMinusNatS3(Succ(wv510), Succ(wv520)) → new_primMinusNatS3(wv510, wv520)
new_primMinusNatS3(Zero, Zero) → Zero
new_primMinusNatS3(Succ(wv510), Zero) → Succ(wv510)

The set Q consists of the following terms:

new_primMinusNatS3(Zero, Zero)
new_primMinusNatS3(Succ(x0), Zero)
new_primMinusNatS3(Succ(x0), Succ(x1))
new_primMinusNatS3(Zero, Succ(x0))

↳ HASKELL

  ↳ IFR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ Narrow

                ↳ AND

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                    ↳ DependencyGraphProof

                      ↳ AND

                        ↳ QDP

                        ↳ QDP

                          ↳ UsableRulesProof

                            ↳ QDP

                              ↳ QReductionProof

                                ↳ QDP

                                  ↳ Rewriting

                                    ↳ QDP

                                      ↳ Rewriting

                                        ↳ QDP

                                          ↳ UsableRulesProof

                                            ↳ QDP

                                              ↳ QReductionProof

                                                ↳ QDP

                                                  ↳ QDPOrderProof

                                                    ↳ QDP

                                                      ↳ DependencyGraphProof

                                                        ↳ QDP

                                                          ↳ UsableRulesProof

                                                            ↳ QDP

                                                              ↳ QReductionProof

Q DP problem:
The TRS P consists of the following rules:

new_primDivNatS0(wv46, wv47, Succ(wv480), Succ(wv490)) → new_primDivNatS0(wv46, wv47, wv480, wv490)

R is empty.
The set Q consists of the following terms:

new_primMinusNatS3(Zero, Zero)
new_primMinusNatS3(Succ(x0), Zero)
new_primMinusNatS3(Succ(x0), Succ(x1))
new_primMinusNatS3(Zero, Succ(x0))

We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.

new_primMinusNatS3(Zero, Zero)
new_primMinusNatS3(Succ(x0), Zero)
new_primMinusNatS3(Succ(x0), Succ(x1))
new_primMinusNatS3(Zero, Succ(x0))

↳ HASKELL

  ↳ IFR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ Narrow

                ↳ AND

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                    ↳ DependencyGraphProof

                      ↳ AND

                        ↳ QDP

                        ↳ QDP

                          ↳ UsableRulesProof

                            ↳ QDP

                              ↳ QReductionProof

                                ↳ QDP

                                  ↳ Rewriting

                                    ↳ QDP

                                      ↳ Rewriting

                                        ↳ QDP

                                          ↳ UsableRulesProof

                                            ↳ QDP

                                              ↳ QReductionProof

                                                ↳ QDP

                                                  ↳ QDPOrderProof

                                                    ↳ QDP

                                                      ↳ DependencyGraphProof

                                                        ↳ QDP

                                                          ↳ UsableRulesProof

                                                            ↳ QDP

                                                              ↳ QReductionProof

                                                                ↳ QDP

                                                                  ↳ QDPSizeChangeProof

Q DP problem:
The TRS P consists of the following rules:

new_primDivNatS0(wv46, wv47, Succ(wv480), Succ(wv490)) → new_primDivNatS0(wv46, wv47, wv480, wv490)

From the DPs we obtained the following set of size-change graphs:

new_primDivNatS0(wv46, wv47, Succ(wv480), Succ(wv490)) → new_primDivNatS0(wv46, wv47, wv480, wv490)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 > 3, 4 > 4

primDivNatS0	x y True	= Succ (primDivNatS (primMinusNatS x y) (Succ y))
primDivNatS0	x y False	= Zero

primModNatS0	x y True	= primModNatS (primMinusNatS x y) (Succ y)
primModNatS0	x y False	= Succ x